$\forall$${\it es}$:ES, $a$:Atom1, $e$:E. $e$ sends $a$ $\in$ Prop